(module unifier  (lib "eopl.ss" "eopl")
  
  (require "drscheme-init.scm")
  (require "lang.scm")
  (require "data-structures.scm")
  (require "substitutions.scm")
  
  ;; this provides a new view of substitutions, in which unifier
  ;; replaces extend-env as a constructor.
  (provide unifier substitution? empty-subst apply-subst-to-type)
  
  ;; we'll maintain the invariant that no variable bound in the
  ;; substitution occurs in any of the right-hand sides of the
  ;; substitution. 
  
  ;;;;;;;;;;;;;;;; the unifier ;;;;;;;;;;;;;;;;
  
  ;;; unifier : type * type * subst * exp -> subst OR fails
  
  (define unifier
    (lambda (ty1 ty2 subst exp)
      (let ((ty1 (apply-subst-to-type ty1 subst))
            (ty2 (apply-subst-to-type ty2 subst)))
        (cond
          ((equal? ty1 ty2) subst)
          ((tvar-type? ty1);;;;if ty1 is an unknown type
           ;; since we've already closed the type, we know that ty1 is
           ;; unbound in subst.
           (if (no-occurrence? ty1 ty2)
               (extend-subst subst ty1 ty2)
               (raise-occurrence-check! ty1 ty2 exp)))
          ((tvar-type? ty2);;;;if ty2 is an unknown type
           (if (no-occurrence? ty2 ty1)
               (extend-subst subst ty2 ty1)
               (raise-occurrence-check! ty2 ty1 exp)))
          ((and (proc-type? ty1) (proc-type? ty2))
           (let ((subst (unifier
                         (proc-type->arg-type ty1)
                         (proc-type->arg-type ty2)
                         subst exp)))
             (let ((subst (unifier
                           (proc-type->result-type ty1)
                           (proc-type->result-type ty2)
                           subst exp)))
               subst)))
          (else (raise-type-error! ty1 ty2 exp))))))
  
  ;; is there an occurrence of tvar in ty?
  (define no-occurrence?
    (lambda (tvar ty)
      (cases type ty
        (proc-type (arg-type result-type)
                   (and
                    (no-occurrence? tvar arg-type)
                    (no-occurrence? tvar result-type)))
        (tvar-type (serial-number) (not (equal? tvar ty)))
        (else #t))))
  
  (define raise-type-error!
    (lambda (t1 t2 exp)
      (eopl:error 'check-equal-type!
                  "Type mismatch: ~s doesn't match ~s in ~s~%"
                  (type-to-external-form t1)
                  (type-to-external-form t2)
                  exp)))
  
  (define raise-occurrence-check!
    (lambda (ty1 ty2 exp)
      (eopl:error 'check-no-occurence!
                  "Can't unify: type variable ~s occurs in type ~s in expression ~s~%" 
                  (type-to-external-form ty1)
                  (type-to-external-form ty2)
                  exp)))
  )